@InProceedings{SilvaAmbrVillAzev:2016:ApVeSa,
               author = "Silva, Pedro and Ambrosio, Ana Maria and Villani, Emilia and 
                         Azevedo, Denise Nunes Rodonti",
          affiliation = "{Instituto Tecnol{\'o}gico de Aeron{\'a}utica (ITA)} and 
                         {Instituto Nacional de Pesquisas Espaciais (INPE)} and {Instituto 
                         Tecnol{\'o}gico de Aeron{\'a}utica (ITA)} and {Instituto 
                         Nacional de Pesquisas Espaciais (INPE)}",
                title = "An approach for verification of a satellite simulator – an 
                         evolving system",
            booktitle = "Proceedings...",
                 year = "2016",
         organization = "Latin-American Symposium on Dependable Computing (LADC)",
             keywords = "Satellite simulator, Test automation, Verification, Validation, 
                         Formal methods, Model checking, Model basedtesting.",
             abstract = "Satellite simulators are developed in the context of a space 
                         mission lifecycle to represent the real behavior of a satellite 
                         during operation and may be used for different purposes. To attend 
                         a particular purpose new functions are added or modified according 
                         to the mission phase needs, requiring models re-adaptation in a 
                         system evolving concept. The process of verification of satellite 
                         simulator software requires high-efficiency in accomplishing 
                         realistic functional and behavioral requirements. Based on the 
                         complex set of requirements the satellite behavior is represented 
                         in the simulator through software models specified by tables of 
                         causeeffect rules. Considering that the Satellite Simulator is an 
                         evolving systems and it needs to assure that the logic implemented 
                         in the simulator conforms to the requirements, the manual 
                         verification process becomes impracticable, therefore demanding a 
                         compatible verification approach. The approach suggested here 
                         unifies two techniques Conformance and Fault Inject (CoFI), 
                         constructed on Model-Based Testing and Model Checking added to a 
                         method so that it can translate the tables of cause-effect rules 
                         into finite state machines. This paper presents the verification 
                         approach illustrating it with the Data Collection Subsystem (DCS) 
                         model of the CBERS satellite simulator being developed at National 
                         Institute for Space Research (INPE).",
  conference-location = "Cali, Colombia",
      conference-year = "19-21 Oct.",
             language = "en",
        urlaccessdate = "27 abr. 2024"
}